event_system{i:l}  Type{i'} 

latex

Definitions	suptype(S; T), subtype(S; T), x,y. t(x;y), x. t(x), top, P  Q, P  Q, x:A. B(x), event_system{i:l}, t  T, x(s1,s2), x(s), prop{i:l}, EOrderAxioms(E;pred?;info), EState(T)
Lemmas	constant function wf, bool wf, qle wf, cless wf, top wf, first wf, assert wf, not wf, val-axiom wf, rationals wf, nat wf, Msg wf, loc wf, kind wf, kindcase wf, Knd wf, EState wf, EOrderAxioms wf, IdLnk wf, Id wf, unit wf, deq wf